Nuprl Definition : l_disjoint
11,40
postcript
pdf
l_disjoint(
T
;
l1
;
l2
) ==
x
:
T
.
((
x
l1
)
(
x
l2
))
latex
clarification:
l_disjoint(
T
;
l1
;
l2
) ==
x
:
T
.
((
x
l1
T
)
(
x
l2
T
))
latex
Definitions
x
:
A
.
B
(
x
)
,
A
,
P
Q
,
(
x
l
)
FDL editor aliases
l_disjoint
origin
x:T. 
((x 
l1) 
(x l2))
x:T. ((x l1 T) (x l2 T)) x:T. ((x l1) (x l2))
x:T. ((x l1 T) (x l2 T)) x:A. B(x)A Q l)